app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
↳ QTRS
↳ DependencyPairsProof
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(f, 0), n) -> APP2(map, f)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(f, 0), n) -> APP2(app2(cons, 0), nil)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(f, 0), n) -> APP2(app2(map, f), app2(app2(cons, 0), nil))
APP2(app2(f, 0), n) -> APP2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
APP2(app2(f, 0), n) -> APP2(cons, 0)
APP2(app2(f, 0), n) -> APP2(hd, app2(app2(map, f), app2(app2(cons, 0), nil)))
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(f, 0), n) -> APP2(map, f)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(f, 0), n) -> APP2(app2(cons, 0), nil)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(f, 0), n) -> APP2(app2(map, f), app2(app2(cons, 0), nil))
APP2(app2(f, 0), n) -> APP2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
APP2(app2(f, 0), n) -> APP2(cons, 0)
APP2(app2(f, 0), n) -> APP2(hd, app2(app2(map, f), app2(app2(cons, 0), nil)))
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(f, 0), n) -> APP2(app2(cons, 0), nil)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(f, 0), n) -> APP2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
APP2(app2(f, 0), n) -> APP2(app2(map, f), app2(app2(cons, 0), nil))
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
Used ordering: Polynomial interpretation [21]:
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(f, 0), n) -> APP2(app2(cons, 0), nil)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(f, 0), n) -> APP2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
APP2(app2(f, 0), n) -> APP2(app2(map, f), app2(app2(cons, 0), nil))
POL(0) = 2
POL(APP2(x1, x2)) = 2·x1
POL(app2(x1, x2)) = 2 + 2·x1·x2
POL(cons) = 0
POL(hd) = 0
POL(map) = 2
POL(nil) = 0
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(f, 0), n) -> APP2(app2(cons, 0), nil)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(f, 0), n) -> APP2(app2(map, f), app2(app2(cons, 0), nil))
APP2(app2(f, 0), n) -> APP2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(f, 0), n) -> app2(app2(hd, app2(app2(map, f), app2(app2(cons, 0), nil))), n)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))